Skip to content

Conversation

@FnControlOption
Copy link
Contributor

Currently, the proof of Theorem 25.9 states that

$$h(f^M(\text{Val}^M_s(t_1),\dots,\text{Val}^M_s(t_n)))$$

is equal to

$$h(f^M(\text{Val}^{M'}_{h \circ s}(t_1),\dots,\text{Val}^{M'}_{h \circ s}(t_n))$$

by the induction hypothesis that

$$h(\text{Val}^M_s(t_i))=\text{Val}^{M'}_{h \circ s}(t_i).$$

However, I'm having difficulty seeing how that is the case.

If instead we use item (5) of Definition 25.8, then we get

$$f^{M'}(h(\text{Val}^M_s(t_1)),\dots,h(\text{Val}^M_s(t_n)))$$

and by the induction hypothesis,

$$f^{M'}(\text{Val}^{M'}_{h \circ s}(t_1),\dots,\text{Val}^{M'}_{h \circ s}(t_n)).$$

@rzach rzach merged commit 94a9dcd into OpenLogicProject:master Nov 22, 2025
1 check passed
@rzach
Copy link
Member

rzach commented Nov 22, 2025

Good catch! Thanks.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants